Trait isotope::ctx::subst::SubstCtx[][src]

pub trait SubstCtx {
    type Ctx: TyCtxMut;
    fn subst_var(
        &mut self,
        ix: u32,
        annot: Option<&TermId>
    ) -> Result<Option<TermId>, Error>;
fn push_param(
        &mut self,
        param_ty: Option<&TermId>
    ) -> Result<Option<TermId>, Error>;
fn intersects(&self, filter: VarFilter, code: Code, form: Form) -> bool;
fn ctx(&mut self) -> &mut Self::Ctx;
fn pop_param(&mut self) -> Result<(), Error>;
fn is_var_null(&self) -> bool; fn cache(
        &mut self,
        _term: &TermId,
        _subst: Option<&TermId>
    ) -> Result<(), Error> { ... }
fn try_subst(
        &mut self,
        _term: &Term
    ) -> Option<Result<Option<TermId>, Error>> { ... }
fn subst_constrain(
        &mut self,
        ix: u32,
        annot: Option<&TermId>
    ) -> Result<Option<TermId>, Error> { ... }
fn cons_ctx(&mut self) -> &mut <Self::Ctx as TyCtxMut>::ConsCtx { ... }
fn eq_ctx(&mut self) -> &mut <Self::Ctx as TyCtxMut>::TermEqCtx { ... }
fn push_param_ctx(&mut self, param_ty: Option<&TermId>) -> Result<(), Error> { ... } }
Expand description

A context for substituting terms

Associated Types

This type’s underlying context

Required methods

Substutite a variable, with an optional un-substituted annotation. Does not add the annotation as a constraint.

Returns an error if the annotation gives a type error. Implementations may return an error when provided a null annotation, or may perform a substitution with no constraint.

Push a parameter onto this context with an optional annotation, returning the annotation substitution, if any

Check whether this context can potentially make any changes to a term with the given filter

Get the underlying context

Pop a parameter from this context

Whether no variables are substituted by this context

Provided methods

Cache a substitution result. May cause erroneous behaviour if the result passed is invalid!

May return an error on invalid input, though this is not guaranteed.

Attempt to substitute an entire term. Return None if substitution should proceed recursively instead.

Substutite a variable, with an optional un-substituted annotation, adding the annotation as a constraint.

Returns an error if the annotation gives a type error. Implementations may return an error when provided a null annotation, or may perform a substitution with no constraint.

Get the underlying consing context

Get the underlying equality context

Push a parameter onto the underlying context with an optional annotation

Implementors